We prove that every computably enumerable random real is provable in Peano Arithmetic to be c.e. random. A major step in the proof is to show that the theorem stating that “a real is c.e. and random iff it is the halting probability of a universal prefix-free Turing machine” can be proven in PA. Our proof, which is simpler than the standard one, can also be used for the original theorem. Our positive result can be contrasted with the case of (...) computable functions, where not every computable function is provably computable in PA, or even more interestingly, with the fact that almost all random finite strings are not provably random in PA. We also prove two negative results: a) there exists a universal machine whose universality cannot be proved in PA, b) there exists a universal machine U such that, based on U, PA cannot prove the randomness of its halting probability. The paper also includes a sharper form of the Kraft-Chaitin Theorem, as well as a formal proof of this theorem written with the proof assistant Isabelle. (shrink)

This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are $${\Delta_1}$$ provably in an arithmetic theory T. In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether $${I\Delta_0 + \neg \mathit{exp}}$$ implies $${B\Sigma_1}$$ to a purely recursion-theoretic question.

This book constitutes the refereed proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory, KGC '97, held in Vienna, Austria, in August 1997. The volume presents 20 revised full papers selected from 38 submitted papers. Also included are seven invited contributions by leading experts in the area. The book documents interdisciplinary work done in the area of computer science and mathematical logics by combining research on provability, analysis of proofs, proof search, and complexity.

We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation between quantified provability logics with respect to \ arithmetical interpretations.

Journal of Mathematical Logic, Volume 22, Issue 03, December 2022. Hirschfeldt and Jockusch (2016) introduced a two-player game in which winning strategies for one or the other player precisely correspond to implications and non-implications between [math] principles over [math]-models of [math]. They also introduced a version of this game that similarly captures provability over [math]. We generalize and extend this game-theoretic framework to other formal systems, and establish a certain compactness result that shows that if an implication [math] between (...) two principles holds, then there exists a winning strategy that achieves victory in a number of moves bounded by a number independent of the specific run of the game. This compactness result generalizes an old proof-theoretic fact noted by H. Wang (1981), and has applications to the reverse mathematics of combinatorial principles. We also demonstrate how this framework leads to a new kind of analysis of the logical strength of mathematical problems that refines both that of reverse mathematics and that of computability-theoretic notions such as Weihrauch reducibility, allowing for a kind of fine-structural comparison between [math] principles that has both computability-theoretic and proof-theoretic aspects, and can help us distinguish between these, for example by showing that a certain use of a principle in a proof is “purely proof-theoretic”, as opposed to relying on its computability-theoretic strength. We give examples of this analysis to a number of principles at the level of [math], uncovering new differences between their logical strengths. (shrink)

Computer simulations and experiments share many important features. One way of explaining the similarities is to say that computer simulations just are experiments. This claim is quite popular in the literature. The aim of this paper is to argue against the claim and to develop an alternative explanation of why computer simulations resemble experiments. To this purpose, experiment is characterized in terms of an intervention on a system and of the observation of the reaction. Thus, if computer simulations are experiments, (...) either the computer hardware or the target system must be intervened on and observed. I argue against the first option using the non-observation argument, among others. The second option is excluded by e.g. the over-control argument, which stresses epistemological differences between experiments and simulations. To account for the similarities between experiments and computer simulations, I propose to say that computer simulations can model possible experiments and do in fact often do so. (shrink)

We determine the strictly positive fragment $\textsf{QPL}^+(\textsf{HA})$ of the quantified provability logic $\textsf{QPL}(\textsf{HA})$ of Heyting Arithmetic. We show that $\textsf{QPL}^+(\textsf{HA})$ is decidable and that it coincides with $\textsf{QPL}^+(\textsf{PA})$, which is the strictly positive fragment of the quantified provability logic of of Peano Arithmetic. This positively resolves a previous conjecture of the authors described in [ 14 ]. On our way to proving these results, we carve out the strictly positive fragment $\textsf{PL}^+(\textsf{HA})$ of the provability logic $\textsf{PL}(\textsf{HA})$ of (...) Heyting Arithmetic, provide a simple axiomatization, and prove it to be sound and complete for two types of arithmetical interpretations. The simple fragments presented in this paper should be contrasted with a recent result by Mojtahedi [ 43 ], where an axiomatization for $\textsf{PL}(\textsf{HA})$ is provided. This axiomatization, although decidable, is of considerable complexity. (shrink)

Information Theory, Evolution and The Origin ofLife: The Origin and Evolution of Life as a Digital Message: How Life Resembles a Computer, Second Edition. Hu- bert P. Yockey, 2005, Cambridge University Press, Cambridge: 400 pages, index; hardcover, US $60.00; ISBN: 0-521-80293-8. The reason that there are principles of biology that cannot be derived from the laws of physics and chemistry lies simply in the fact that the genetic information content of the genome for constructing even the simplest organisms is much (...) larger than the information content of these laws. Yockey in his previous book (1992, 335) In this new book, Information Theory, Evolution and The Origin ofLife, Hubert Yockey points out that the digital, segregated, and linear character of the genetic information system has a fundamental significance. If inheritance would blend and not segregate, Darwinian evolution would not occur. If inheritance would be analog, instead of digital, evolution would be also impossible, because it would be impossible to remove the effect of noise. In this way, life is guided by information, and so information is a central concept in molecular biology. The author presents a picture of how the main concepts of the genetic code were developed. He was able to show that despite Francis Crick's belief that the Central Dogma is only a hypothesis, the Central Dogma of Francis Crick is a mathematical consequence of the redundant nature of the genetic code. The redundancy arises from the fact that the DNA and mRNA alphabet is formed by triplets of 4 nucleotides, and so the number of letters (triplets) is 64, whereas the proteome alphabet has only 20 letters (20 amino acids), and so the translation from the larger alphabet to the smaller one is necessarily redundant. Except for Tryptohan and Methionine, all amino acids are coded by more than one triplet, therefore, it is undecidable which source code letter was actually sent from mRNA. This proof has a corollary telling that there are no such mathematical constraints for protein-protein communication. With this clarification, Yockey contributes to diminishing the widespread confusion related to such a central concept like the Central Dogma. Thus the Central Dogma prohibits the origin of life "proteins first." Proteins can not be generated by "self-organization." Understanding this property of the Central Dogma will have a serious impact on research on the origin of life. (shrink)

Given any simply consistent formal theory F of the state complexity L(S) of finite binary sequences S as computed by 3-tape-symbol Turing machines, there exists a natural number L(F ) such that L(S) > n is provable in F only if n L(F ). The proof resembles Berry’s..

We give a self-contained and streamlined version of the classification of the provably computable functions of PA. The emphasis is put on illuminating as well as seems possible the intrinsic computational character of the standard cut elimination process. The article is intended to be suitable for teaching purposes and just requires basic familiarity with PA and the ordinals below ε0. (Familiarity with a cut elimination theorem for a Gentzen or Tait calculus is helpful but not presupposed).

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

In this paper, we discuss semantical properties of the logic $\textbf{GL}$ of provability. The logic $\textbf{GL}$ is a normal modal logic which is axiomatized by the the Löb formula $\Box (\Box p\supset p)\supset \Box p$, but it is known that $\textbf{GL}$ can also be axiomatized by an axiom $\Box p\supset \Box \Box p$ and an $\omega$ -rule $(\Diamond ^{*})$ which takes countably many premises $\phi \supset \Diamond ^{n}\top$ $(n\in \omega )$ and returns a conclusion \(\phi (...) \supset \bot \). We show that the class of transitive Kripke frames which validates $(\Diamond ^{*})$ and the class of transitive Kripke frames which strongly validates $(\Diamond ^{*})$ are equal, and that the following three classes of transitive Kripke frames, the class which validates $(\Diamond ^{*})$, the class which weakly validates $(\Diamond ^{*})$, and the class which is defined by the Löb formula, are mutually different, while all of them characterize $\textbf{GL}$. This gives an example of a proof system _P_ and a class _C_ of Kripke frames such that _P_ is sound and complete with respect to _C_ but the soundness cannot be proved by simple induction on the height of the derivations in _P_. We also show Kripke completeness of the proof system with $(\Diamond ^{*})$ in an algebraic manner. As a corollary, we show that the class of modal algebras which is defined by equations $\Box x\le \Box \Box x$ and $\bigwedge _{n\in \omega }\Diamond ^{n}1=0$ is not a variety. (shrink)

We present a semantic game for Gödel logic and its extensions, where the players’ interaction stepwise reduces arbitrary claims about the relative order of truth degrees of complex formulas to atomic ones. The paper builds on a previously developed game for Gödel logic with projection operator in Fermüller et al., Information processing and management of uncertainty in knowledge-based systems, Springer, Cham, 2020, pp. 257–270). This game is extended to cover Gödel logic with involutive negations and constants, and then lifted to (...) a provability game using the concept of disjunctive strategies. Winning strategies in the provability game, with and without constants and involutive negations, turn out to correspond to analytic proofs in a version of \ :1941–1958, 2010) and in a sequent-of-relations calculus, Automated reasoning with analytic tableaux and related methods, Springer, Berlin, 1999, pp. 36–51) respectively. (shrink)

This chapter draws an analogy between computing mechanisms and autopoietic systems, focusing on the non-representational status of both kinds of system (computational and autopoietic). It will be argued that the role played by input and output components in a computing mechanism closely resembles the relationship between an autopoietic system and its environment, and in this sense differs from the classical understanding of inputs and outputs. The analogy helps to make sense of why we should think of computing mechanisms as non-representational, (...) and might also facilitate reconciliation between computational and autopoietic/enactive approaches to the study of cognition. (shrink)

We will investigate patterns of resemblance of order 2 over a family of arithmetic structures on the ordinals. In particular, we will show that they determine a computable well ordering under appropriate assumptions.

Architecture often relies on mathematical models, if only to anticipate the physical behavior of structures. Accordingly, mathematical modeling serves to find an optimal form given certain constraints, constraints themselves translated into a language which must be homogeneous to that of the model in order for resolution to be possible. Traditional modeling tied to design and architecture thus appears linked to a topdown vision of creation, of the modernist, voluntarist and uniformly normative type, because usually (mono)functionalist. One available instrument of calculation/representation/prescription (...) orders this conception of architecture: indeed the search for an optimal solution through mathematical calculation of a model itself mathematical, thus homogeneous and simple, is only possible when one or two functions or functional constraints are formulated, never more, and this, on a global level, therefore starting from a unique and homogenizing viewpoint. It is essential to grasp that, even applied to material and its properties or towards a particular esthetic or functional dimension, this viewpoint is thus abstractive and generalizing: disregarding singularity of context, insertion and relationship to the environment or local, social behavior. It leaves aside functional specificity and heterogeneousness – re-contextualized each time – of functions that the object or edifice are required to fulfill and optimize under diverse constraints, in their different parts. The computational turning point today’s digital design and computational architecture embody modifies these instrumental, original prescriptions, rendering them more flexible. Perhaps in light of this turnabout we should retrospectively interpret 20th century calls for modernism, functionalism and even biomorphism as being just as many ex post rationalizations in respect to techniques of strongly prescriptive modeling since our only instrument is a monolithic language, and so being, incites a top-down conception, (naturally weakly reactive to contexts), including forms whose overall appearance resembles in fine a living form. In order to liberate oneself from this and despite everything, emerge as its initiators, one has constructed from ideology and philosophy (of object, habitat, the urban) ex post, even while it is the instrument of modeling and conception that largely determines, normalizes and dictates ex ante, the possibilities and limitations of the creation of forms and living experiments4 in a given time. (shrink)

We compare our model of unsupervised learning of linguistic structures, ADIOS [1, 2, 3], to some recent work in computational linguistics and in grammar theory. Our approach resembles the Construction Grammar in its general philosophy (e.g., in its reliance on structural generalizations rather than on syntax projected by the lexicon, as in the current generative theories), and the Tree Adjoining Grammar in its computational characteristics (e.g., in its apparent affinity with Mildly Context Sensitive Languages). The representations learned by our algorithm (...) are truly emergent from the (unannotated) corpus data, whereas those found in published works on cognitive and construction grammars and on TAGs are hand-tailored. Thus, our results complement and extend both the computational and the more linguistically oriented research into language acquisition. We conclude by suggesting how empirical and formal study of language can be best integrated. (shrink)

In this paper, we discuss semantical properties of the logic $\textbf{GL}$ of provability. The logic $\textbf{GL}$ is a normal modal logic which is axiomatized by the the Löb formula $\Box (\Box p\supset p)\supset \Box p$, but it is known that $\textbf{GL}$ can also be axiomatized by an axiom $\Box p\supset \Box \Box p$ and an $\omega$ -rule $(\Diamond ^{*})$ which takes countably many premises $\phi \supset \Diamond ^{n}\top$ $(n\in \omega )$ and returns a conclusion \(\phi (...) \supset \bot \). We show that the class of transitive Kripke frames which validates $(\Diamond ^{*})$ and the class of transitive Kripke frames which strongly validates $(\Diamond ^{*})$ are equal, and that the following three classes of transitive Kripke frames, the class which validates $(\Diamond ^{*})$, the class which weakly validates $(\Diamond ^{*})$, and the class which is defined by the Löb formula, are mutually different, while all of them characterize $\textbf{GL}$. This gives an example of a proof system _P_ and a class _C_ of Kripke frames such that _P_ is sound and complete with respect to _C_ but the soundness cannot be proved by simple induction on the height of the derivations in _P_. We also show Kripke completeness of the proof system with $(\Diamond ^{*})$ in an algebraic manner. As a corollary, we show that the class of modal algebras which is defined by equations $\Box x\le \Box \Box x$ and $\bigwedge _{n\in \omega }\Diamond ^{n}1=0$ is not a variety. (shrink)

Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of classical mathematics is rather restricted in scope due to the existence of sentences without computational content which are provable from the law of excluded middle and which involve only two quantifier alternations. By contrast, we show that the proof mining of classical Nonstandard Analysis has a very (...) large scope. In particular, we will observe that this scope includes any theorem of pure Nonstandard Analysis, where 'pure' means that only nonstandard definitions are used. In this note, we survey results in analysis, computability theory, and Reverse Mathematics. (shrink)

We study interpolation properties for Shavrukov’s bimodal logic $$\textbf{GR}$$ of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic $$\textbf{GR}^\circ$$ of $$\textbf{GR}$$ and its relational semantics. Based on our new semantics, we prove that $$\textbf{GR}^\circ$$ and $$\textbf{GR}$$ enjoy Lyndon interpolation property and uniform interpolation property. As a consequence of our proofs, we obtain the completeness and the finite frame property of $$\textbf{GR}^\circ$$ and $$\textbf{GR}$$ with respect to our new semantics.

This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). In the (...) resulting theory we show the extractability of primitive recursive programs and uniform bounds from proofs of $\forall\exists$-theorems. There are two components of this work. The first component is a general proof-theoretic result, due to the second author, that establishes conservation results for restricted principles of choice and comprehension over primitive recursive arithmetic PRA as well as a method for the extraction of primitive recursive bounds from proofs based on such principles. The second component is the main novelty of the paper: it is shown that a proof of Ramsey's theorem due to Erdős and Rado can be formalized using these restricted principles. So from the perspective of proof unwinding the computational content of concrete proofs based on $RT^2_2$ the computational complexity will, in most practical cases, not go beyond primitive recursive complexity. This even is the case when the theorem to be proved has function parameters f and the proof uses instances of $RT^2_2$ that are primitive recursive in f. (shrink)

The world of artificial intelligence appears to be in rapid transition, and claims that artificial general intelligence is impossible are competing with concerns that we may soon be seeing Artificial Godlike Intelligence and that we should be very afraid of this prospect. This article discusses the issues from a psychological and social perspective and suggests that with the advent of Generative Artificial Intelligence, something that looks to humans like Artificial General Intelligence has become a distinct possibility as is the idea (...) of making it semi-autonomous: not just responding to discrete external inputs or performing specific tasks but able to prompt itself to create an ongoing stream of cognition that can possess something akin to a ‘purpose’. Add to that the ability of computers to be connected in vast networks, and we can envisage intelligences with staggering amounts of knowledge and reasoning capability, engaging with humans to anticipate and grant wishes. Such Semi-Autonomous Godlike Artificial Intelligences (SAGAIs—meaning ‘engagements’ in Hindi) could end up like Kali, wreaking death and destruction on our species or like Thor, acting as a saviour and protector of humanity. Which of these our SAGAIs most resemble could depend on whose wishes it is designed to serve: a rich oligarchy seeking ever greater wealth and power whatever the cost to others, or a populace that has compassion for each other and for life on the planet. (shrink)

N. Bostrom’s simulation argument and two additional assumptions imply that we likely live in a computer simulation. The argument is based upon the following assumption about the workings of realistic brain simulations: The hardware of a computer on which a brain simulation is run bears a close analogy to the brain itself. To inquire whether this is so, I analyze how computer simulations trace processes in their targets. I describe simulations as fictional, mathematical, pictorial, and material models. Even though the (...) computer hardware does provide a material model of the target, this does not suffice to underwrite the simulation argument because the ways in which parts of the computer hardware interact during simulations do not resemble the ways in which neurons interact in the brain. Further, there are computer simulations of all kinds of systems, and it would be unreasonable to infer that some computers display consciousness just because they simulate brains rather than, say, galaxies. (shrink)

In this paper we will state and prove some comparative theorems concerning PRA and IΣ1. We shall provide a characterization of IΣ1 in terms of PRA and iterations of a class of functions. In particular, we prove that for this class of functions the difference between IΣ1 and PRA is exactly that, where PRA is closed under iterations of these functions, IΣ1 is moreover provably closed under iteration. We will formulate a sufficient condition for a model of PRA to be (...) a model of IΣ1. This condition is used to give a model-theoretic proof of Parsons’ theorem, that is, IΣ1 is Π2-conservative over PRA. We shall also give a purely syntactical proof of Parsons’ theorem. Finally, we show that IΣ1 proves the consistency of PRA on a definable IΣ1-cut. This implies that proofs in IΣ1 can have non-elementary speed up over proofs in PRA. (shrink)

What did science make possible for colonial rule? How was science in turn marked by the knowledge and practices of those under colonial rule? Here I approach these questions via the social history of Madras Observatory. Constructed in 1791 by the East India Company, the observatory was to provide local time to mariners and served as a clearinghouse for the company’s survey and revenue administration. The astronomical work of Madras’ Brahmin assistants relied upon their knowledge of jyotiśāstra [Sanskrit astronomy/astrology], and (...) can be seen as a specialized form of the kind of South Indian scribal labor and knowledge that also staffed the company’s tax offices. If at Greenwich the division of labor meant observatory work bore resemblances to the factory and the accounts office, in Madras, astronomy and accounting drew on similar labor forms because they were part of the same enterprise. But the company did not just adapt preexisting forms of labor, it also attempted to produce its own at a school built near the observatory to train “half-caste” orphans as apprentice surveyors and assistant computers. The school, staffed by the Brahmins, drew upon knowledge and pedagogical practice associated with the tinnai, the schools in which upper-caste children learned to read, write, and calculate. For a time, the observatory’s social order was literally “half-caste.” The paper also considers how the relationship between caste, status, and instrument was reflected in the visual and material culture of the observatory, such as in Indian-language inscriptions on its central pillar. For company astronomers, the measurement of time meant reworking the relationships among the Indian past, the colonial present, and an imperial posterity. Science under colonial rule spanned multiple temporal and social registers because it was the result of negotiations between the demands of political economy and the knowledge and practices of colonized others. (shrink)

monsters, virtual legends such as 2001’s HAL or Demon Seed’s Proteus are actually scary because of their mind. Without lingering on the philosophical debates on whether a certain type of mind can exist independent of its specific embodiment or whether any creature can understand a consciousness that is not like his own (recall Lem’s Solaris), the thing that makes HAL and Proteus so human is not so much their ability to think as their possessing something resembling human consciousness. The (...) point is that, whereas consciousness may or may not be required for an artificial agent to think, it is an essential element in creating anything resembling a human-like thinker that would pass the Turing Test. (shrink)

We study randomness beyond${\rm{\Pi }}_1^1$-randomness and its Martin-Löf type variant, which was introduced in [16] and further studied in [3]. Here we focus on a class strictly between${\rm{\Pi }}_1^1$and${\rm{\Sigma }}_2^1$that is given by the infinite time Turing machines introduced by Hamkins and Kidder. The main results show that the randomness notions associated with this class have several desirable properties, which resemble those of classical random notions such as Martin-Löf randomness and randomness notions defined via effective descriptive set theory such as${\rm{\Pi (...) }}_1^1$-randomness. For instance, mutual randoms do not share information and a version of van Lambalgen’s theorem holds.Towards these results, we prove the following analogue to a theorem of Sacks. If a real is infinite time Turing computable relative to all reals in some given set of reals with positive Lebesgue measure, then it is already infinite time Turing computable. As a technical tool towards this result, we prove facts of independent interest about random forcing over increasing unions of admissible sets, which allow efficient proofs of some classical results about hyperarithmetic sets. (shrink)

A practical viewpoint links reality, representation, and language to calculation by the concept of Turing (1936) machine being the mathematical model of our computers. After the Gödel incompleteness theorems (1931) or the insolvability of the so-called halting problem (Turing 1936; Church 1936) as to a classical machine of Turing, one of the simplest hypotheses is completeness to be suggested for two ones. That is consistent with the provability of completeness by means of two independent Peano arithmetics discussed in Section (...) I. Many modifications of Turing machines cum quantum ones are researched in Section II for the Halting problem and completeness, and the model of two independent Turing machines seems to generalize them. Then, that pair can be postulated as the formal definition of reality therefore being complete unlike any of them standalone, remaining incomplete without its complementary counterpart. Representation is formal defined as a one-to-one mapping between the two Turing machines, and the set of all those mappings can be considered as “language” therefore including metaphors as mappings different than representation. Section III investigates that formal relation of “reality”, “representation”, and “language” modeled by (at least two) Turing machines. The independence of (two) Turing machines is interpreted by means of game theory and especially of the Nash equilibrium in Section IV. Choice and information as the quantity of choices are involved. That approach seems to be equivalent to that based on set theory and the concept of actual infinity in mathematics and allowing of practical implementations. (shrink)

Provability, Computability and Reflection.

This contribution defends two claims. The first is about why thought experiments are so relevant and powerful in mathematics. Heuristics and proof are not strictly and, therefore, the relevance of thought experiments is not contained to heuristics. The main argument is based on a semiotic analysis of how mathematics works with signs. Seen in this way, formal symbols do not eliminate thought experiments (replacing them by something rigorous), but rather provide a new stage for them. The formal world resembles the (...) empirical world in that it calls for exploration and offers surprises. This presents a major reason why thought experiments occur both in empirical sciences and in mathematics. The second claim is about a looming aporia that signals the limitation of thought experiments. This aporia arises when mathematical arguments cease to be fully accessible, thus violating a precondition for experimenting in thought. The contribution focuses on the work of Vladimir Voevodsky (1966–2017, Fields medalist in 2002) who argued that even very pure branches of mathematics cannot avoid inaccessibility of proof. Furthermore, he suggested that computer verification is a feasible path forward, but only if proof is not modeled in terms of formal logic. (shrink)

Many researchers insist that computational methods will transform the historical profession, while an equally large number reject these claims as unwarranted hype. This study attempts to place the debate in historical and social context. The essay is divided into three parts. The first part offers a brief review of computational history. It asks whether the “computational turn” bears any resemblance to quantitative history and how it fits within the digital humanities. The second part describes the authors’ recent attempts to apply (...) computational methods to an existing project in the history of science using a standardized workflow. It demonstrates that each step of the workflow adds another layer of subjectivity. The third part reflects on what computational methods mean for the historical profession. It systematically reviews the positive aspects of computational history (open access, interdisciplinary collaboration, and new perspectives) as well as the negative aspects (inequality, fragility, and the threat of automation) and offers prescriptions based on the authors’ experiences. (shrink)

1. Setting off: An introduction. 1.1. A measure of motivation. 1.2. Computable mathematics. 1.3. Reverse mathematics. 1.4. An overview. 1.5. Further reading -- 2. Gathering our tools: Basic concepts and notation. 2.1. Computability theory. 2.2. Computability theoretic reductions. 2.3. Forcing -- 3. Finding our path: Konig's lemma and computability. 3.1. II[symbol] classes, basis theorems, and PA degrees. 3.2. Versions of Konig's lemma -- 4. Gauging our strength: Reverse mathematics. 4.1. RCA[symbol]. 4.2. Working in RCA[symbol]. 4.3. ACA[symbol]. 4.4. (...) WKL[symbol]. 4.5. [symbol]-models. 4.6. First order axioms. 4.7. Further remarks -- 5. In defense of disarray -- 6. Achieving consensus: Ramsey's theorem. 6.1. Three proofs of Ramsey's theorem. 6.2. Ramsey's theorem and the arithmetic hierarchy. 6.3. RT, ACA[symbol], and the Paris-Harrington theorem. 6.4. Stability and cohesiveness. 6.5. Mathias forcing and cohesive sets. 6.6. Mathias forcing and stable colorings. 6.7. Seetapun's theorem and its extensions. 6.8. Ramsey's theorem and first order axioms. 6.9. Uniformity -- 7. Preserving our power: Conservativity. 7.1. Conservativity over first order systems. 7.2. WKL[symbol] and II[symbol]-conservativity. 7.3. COH and r-II[symbol]-conservativity -- 8. Drawing a map: Five diagrams -- 9. Exploring our surroundings: The world below RT[symbol]. 9.1. Ascending and descending sequences. 9.2. Other combinatorial principles provable from RT[symbol]. 9.3. Atomic models and omitting types -- 10. Charging ahead: Further topics. 10.1. The Dushnik-Miller theorem. 10.2. Linearizing well-founded partial orders. 10.3. The world above ACA[symbol]. 10.4. Still further topics, and a final exercise. (shrink)

Hubert Dreyfus once noted that it would be difficult to ascertain whether Edmund Husserl had a computational theory of mind. I provide evidence that he had one. Both Steven Pinker and Steven Horst think that the computational theory of mind must have two components: a representational-symbolic component and a causal component. Bearing this in mind, we proceed to a close-reading of the sections of “On the Logic of Signs” wherein Husserl presents, if I’m correct, his computational theory of mind embedded (...) in a language of thought. My argument goes like this: the computational theory of mind is the idea, following Haugeland, that the mind comes prepackaged as, or is endogenously constrained to be, an automatic formal system; this explains, according to Husserl, why automatic trains of thought without logical intent resemble arguments exhibiting deductive structure with logical intent. In general, an automatic formal system yields true results provided that the syntactic symbols with which they compute are univocal and are semantically evaluable, and the mechanized inferences they perform are valid and preserve truth. These two conditions describe a computational cognitive process: the first condition connects representations to syntax, and the second condition uses the syntax, in inauthentic judging, to arrive at true conclusions through blind causality. Now, in point of textual fact, these are the conditions which Husserl attributes to our “natural psychological mechanism of symbolic inference” which typically yields true results. Since a formal system attributed to the “internal structure” of the mind, and guided by blind causality, just is the computational theory of mind, it follows, I think, that Husserl had a computational theory of mind. This computational theory is, moreover, embedded in a language of thought, since Husserl attributes a language-like form to our thoughts so that they may be mechanically processed. I conclude with a discussion of my results. (shrink)

Viewed from an evolutionary standpoint, emotions can be understood as situation-specific patterns of energy consumption related to behaviors that have been selected by evolution for their survival value, such as environmental exploration, flight or fight, and socialization. In the present article, the energy linked with emotions is investigated by a strictly energy-based simulation of the evolution of simple autonomous agents provided with random cognitive and motor capacities and operating among food and predators. Emotions are translated into evolving patterns of energy (...) consumption related to situation-specific behaviors. As a result, a variety of behaviors resembling emotions emerge, each with a specific pattern of energy consumption. There is little difference between emotion-like behaviors on individual and collective levels. The fact that these patterns evolve under a strictly energetic selection regime indicates the interesting role and adaptive advantage of emotions as situation-specific energy savers. Although gained through an approach characterized by a highly reduced complexity, these findings support a quantitative understanding of emotions that may improve the existing qualitative approaches and could have far-reaching implications for further research on and conceptualization of emotions and their interactions with cognition. (shrink)

On the one hand, we think that our conscious perceptions are tied to some stage of whatever processing stream we have. On the other hand, we think that our conscious experiences have to resemble the computational states that instantiate them. However, nothing in our alleged stream resembles our experienced perceptions. Hence, a conflict. The question is: How can we go from what we know about neurons, their connections, and firing patterns, to explaining what conscious perceptual experiences are like? No intuitive (...) answer seems plausible. Our perceptual experiences are complex and unified; however, brains divide their processing tasks into small chunks and segregate those smaller pieces across the gray matter. In this essay, I conjecture that what corresponds to our visual perceptions are higher order patterns of bifurcation in an attractor phase space. If I am correct, then the problem of the explanatory gap in philosophy, the binding problem in psychology, and the problem of perception in neuroscience disappear. If the traditional computational perspective is wrong, and sensory processing is not piece-meal, step-wise, and segregated, then there is no need for something in the head to tie things together. (shrink)

Computational imagination (CI) conceives imagination as an agent’s simulated sensorimotor interaction with the environment in the absence of sensory feedback, predicting consequences based on this interaction (Marques and Holland in Neurocomputing 72:743–759, 2009). Its bedrock is the simulation hypothesis whereby imagination resembles seeing or doing something in reality as both involve similar neural structures in the brain (Hesslow in Trends Cogn Sci 6(6):242–247, 2002). This paper raises two-forked doubts: (1) neural-level equivalence is escalated to make phenomenological equivalence. Even at an (...) abstract level, many imagined and real actions turn out to be dissimilar. More so, some imagined actions have no corresponding real actions and vice versa, even though neural regions involved in imaginings and real action-perception are the same (Sect. 1). (2) At the implementation level, the hypothesis presents a mutually exclusive view of imagination and perception whereby imagination functions in the absence of the sensory feedback and is action based. Both these issues are contested here: Neither imagination functions in the absence of perception nor all forms of imaginings are action based; it is, rather, about conceiving possibilities which emerge during the perceptual stage itself (Sect. 2). For the modal aspect to arise, it is submitted that an integrative framework is required which Kant can provide for whom imagination is an indispensable part of perception. Kant’s views on concept-formation are presented here to illustrate this aspect (Sect. 3). The Paper is concluded with emphasizing the relevance of Kant’s views to the problems identified in the two sections. (shrink)

Two general features of metameric patterning in Drosophilaare considered: (1) maintenance of a constant number of metameres (segments or parasegments) in the face of variation in length of the embryo; (2) expression of pattern by on‐off switchings of particular genes, with only three or four rows of cells to each element of pattern. For each of these features, the general strategic question is raised: could reaction‐diffusion theory account for this? In both cases, it is answered affirmatively. For the second feature, (...) this review contains some hitherto unpublished computer simulations by one of us (K. Y. T.), illustrating that a reaction‐diffusion mechanism can be transformed into a patterned switching mechanism by nothing more than compartmenting of the diffusion region. For the scale of three compartments to one pattern repeat unit (representing three rows of cells to a segment) the switching pattern predicted by computation is two‐off to one‐on. This resembles the pattern of expression of the engrailed gene, posteriorly localized in each segment. (shrink)

Provability, Computability and Reflection.

We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the (...) variable-free fragment of GLP Λ. (shrink)

Looking back on the development of computer technology, particularly in the context of manufacturing, we can distinguish three big waves of technological exuberance with a wave length of roughly 30 years: In the first wave, during the 1950s, mainframe computers at that time were conceptualized as “electronic brains” and envisaged as central control unit of an “automatic factory”. Thirty years later, during the 1980s, knowledge-based systems in computer-integrated manufacturing were adored as the computational core of the “unmanned factory”. Both waves (...) dismally stranded on the contumacies of reality. Nevertheless, again thirty years later, we now experience the departure of the “smart factory” based on networks of “artificially intelligent” multi-agent or “cyber-physical systems”. From the very beginning, these technological exuberances rooted in mistaken metaphors describing the artifacts and, hence, in delusions about the true nature of computer systems. The behaviour of computers is, as computing science teaches us, strictly restrained to executing computable functions by means of algorithms, it thus neither resembles the performance of a brain as part of a complex sensitive living body nor is it in any meaningful sense “knowledgeable” or “intelligent”. When the delusion of being able to implement “smart factories”, despite the countless accomplishment failures before, gains momentum anew, it appears absolutely essential to reflect on underlying misconceptions. (shrink)

I hold up my hand and I count five fingers. I take it on faith that the mapping from fingers onto numbers is recursive in the sense of the mathematician’s definition of the informal concept, “human calculability following a fixed routine.” I cannot prove the mapping is recursive—there is nothing to prove! Of course, mathematicians can prove many theorems about recursiveness, moving forward, so to speak, once the definition of the concept “recursive” has been isolated. Moving backwards is more difficult (...) and this is as it should be: for how can one possibly hope to prove that a mathematical definition captures an informal concept? This paper is about just that one word, capture, or more precisely the rela- tion “x captures y,” and the question, if y is taken to be computability, definabil- ity or provability, does there exist an adequate and unique choice of x? (shrink)

In previous work we gave a new proof-theoretical method for establishing upper-bounds on the space complexity of the provability problem of modal and other propositional non-classical logics. Here we extend and refine these results to give an O -space decision procedure for the basic positive relevance logic B+. We compute this upper-bound by first giving a sound and complete, cut-free, labelled sequent system for B+, and then establishing bounds on the application of the rules of this system.

One recursively enumerable real α dominates another one β if there are nondecreasing recursive sequences of rational numbers (a[n] : n ∈ ω) approximating α and (b[n] : n ∈ ω) approximating β and a positive constant C such that for all n, C(α − a[n]) ≥ (β − b[n]). See [R. M. Solovay, Draft of a Paper (or Series of Papers) on Chaitin’s Work, manuscript, IBM Thomas J. Watson Research Center, Yorktown Heights, NY, 1974, p. 215] and [G. J. (...) Chaitin, IBM J. Res. Develop., 21 (1977), pp. 350–359]. We show that every recursively enumerable random real dominates all other recursively enumerable reals. We conclude that the recursively enumerable random reals are exactly the Ω-numbers [G. J. Chaitin, IBM J. Res. Develop., 21 (1977), pp. 350–359]. Second, we show that the sets in a universal Martin-Lof test for randomness have random measure, and every recursively enumerable random number is the sum of the measures represented in a universal Martin-Lof test. (shrink)

In his article “On Mechanical Recognition” R. J. Nelson brings to bear a branch of mathematical logic called automata theory on problems of artificial intelligence. Specifically he attacks the anti-mechanist claim that “[i]nasmuch as human recognition to a very great extent relies on context and on the ability to grasp wholes with some independence of the quality of the parts, even to fill in the missing parts on the basis of expectations, it follows that computers cannot in principle be programmed (...) to recognize or learn to recognize all patterns”, p. 24). Nelson proposes, contrary to this claim, that “gestalt recognition is not beyond digital automata”. in particular, he claims, he will establish by what he calls “Turing machine arguments” that the following four theses are true: automata can recognize different pattern types in one and the same set of instances;automata can recognize the “same” pattern in different sets of instances;automata can recognize incomplete, degraded patterns having missing or indeterminate parts;automata can recognize family resemblances. (shrink)

Decision makers often rely on expert opinion when making forecasts under uncertainty. In doing so, they confront two methodological challenges: the elicitation problem, which requires them to extract meaningful information from experts; and the aggregation problem, which requires them to combine expert opinion by resolving disagreements. Linear averaging is a justifiably popular method for addressing aggregation, but its robust simplicity makes two requirements on elicitation. First, each expert must offer probabilistically coherent forecasts; second, each expert must respond to all our (...) queries. In practice, human judges (even experts) may be incoherent, and may prefer to assess only the subset of events about which they are comfortable offering an opinion. In this paper, a new methodology is developed for combining expert assessment of chance. The method retains the conceptual and computational simplicity of linear averaging, but generalizes the standard approach by relaxing the requirements on expert elicitation. The method also enjoys provable performance guarantees, and in experiments with real-world forecasting data is shown to offer both computational efficiency and competitive forecasting gains as compared to rival aggregation methods. This paper is relevant to the practice of decision analysis, for it enables an elicitation methodology in which judges have freedom to choose the events they assess. (shrink)